Nuprl Lemma : es-pred-locl 11,40
the_es:event_system{i:l}, j:es-E(the_es).
((es-first(the_es; j)))  es-locl(the_es; es-pred(the_es; j); j) 
latex

Definitionsx:A. B(x), P  Q, t  T, P  Q, prop{i:l}
Lemmases-axioms, not wf, assert wf, es-first wf, es-E wf, event system wf

origin